\begin{tabbing}
recognizer{-}p(${\it es}$;$T$;$A$;$P$;$k$;$i$;$r$;$x$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$e$@$i$. (kind($e$) = $k$) $\Rightarrow$ (valtype($e$) $\subseteq$r $T$) \& (vartype($i$;$x$) $\subseteq$r $A$)\+
\\[0ex]\& @$i$($r$:$\mathbb{B}$)
\\[0ex]\& $\forall$$e$@$i$. ($\uparrow$first($e$)) $\Rightarrow$ (($r$ when $e$) = ff)
\\[0ex]\& \=$\forall$$e$@$i$.\+
\\[0ex]($\uparrow$($r$ after $e$))
\\[0ex]$\Leftarrow\!\Rightarrow$ ($\exists$${\it e'}$:E. ((${\it e'}$ $\leq$loc $e$  \& kind(${\it e'}$) = $k$) c$\wedge$ ($\uparrow$($P$(($x$ when ${\it e'}$),val(${\it e'}$))))))
\-\-
\end{tabbing}